
from chaotic_ex import chaotic_ex
from interval import State, bottom, top, assign, force_range, force_less, iota, Range, ScanfExp, AddConstExp, ConstExp, force_exclude_from_range, Inf, inf

succ = {
    0: set([1]),
    1: set([2]),
    2: set([3]),
    3: set([4]),
    4: set([5]),
    5: set([6,30]),
    6: set([7, 15, 21, 26]),
    7: set([8, 10]),
    8: set([9]),
    9: set([30]),
    10: set([11]),
    11: set([12]),
    12: set([13]),
    13: set([14]),
    14: set([4]),
    15: set([16, 18]),
    16: set([17]),
    17: set([30]),
    18: set([19]),
    19: set([20]),  
    20: set([4]),
    21: set([22]),
    22: set([23,25]),
    23: set([24]),
    24: set([22]),
    25: set([4]),
    26: set([27]),
    27: set([30]),
    28: set([4]),
    29: set([]),
    30: set([])
    } # CFG edges


EOF = 0xff
nop = lambda state: state
tr = {
    (0, 1): lambda state: assign(state, 'top', ConstExp(0)),
    (1, 2): nop,
    (2, 3): lambda state: assign(state, 'size', ScanfExp()),
    (3, 4): nop,
    (4, 5): lambda state: assign(state, 'kind', ScanfExp()),
    (5, 6): lambda state: force_exclude_from_range(state, 'kind', EOF),
    (5, 30): lambda state: force_range(state, 'kind', Range(EOF,EOF)),
    (6, 7): lambda state: force_range(state, 'kind', Range(0,0)),
    (7, 8): lambda state: force_less(state, 'size', 'top', equal=True),
    (8, 9): nop,
    (9, 30): nop,
    (7, 10): lambda state: force_less(state, 'top', 'size'),
    (10, 11): nop,
    (11, 12): lambda state: assign(state, 'data', ScanfExp()),
    (12, 13): nop,#'stack[top] = data',
    (13, 14): lambda state: assign(state, 'top', AddConstExp('top', 1)),
    (14, 4): nop,
    (6, 15): lambda state: force_range(state, 'kind', Range(1,1)),
    (15, 16): lambda state: force_range(state, 'top', Range(inf,0)),
    (16, 17): nop,
    (17, 30): nop,
    (15, 18): lambda state: force_range(state, 'top', Range(1,Inf)),
    (18, 19): lambda state: assign(state, 'top', AddConstExp('top', -1)),
    (19, 20): nop,
    (20, 4): nop,
    (6, 21): lambda state: force_range(state, 'kind', Range(2,2)),
    (21, 22): lambda state: assign(state, 'i', ConstExp(0)),
    (22, 23): lambda state: force_less(state, 'i', 'top'), #'i < top',
    (23, 24): nop,
    (24, 22): lambda state: assign(state, 'i', AddConstExp('i',1)),
    (22, 25): lambda state: force_less(state, 'top', 'i', equal=True), #'i >= top',
    (25, 4): nop,
    (6, 26): lambda state: force_range(state, 'kind', Range(3,Inf)),
    (26, 27): nop,
    (27, 30): nop,
    (28, 4): nop,
    } # transfer function

tr_txt  = {
    (0, 1): "top = 0 ;",
    (1, 2): 'fprintf(stderr, "enter maximum stacks size");',
    (2, 3): 'scanf("d", &size);',
    (3, 4): 'stack = (int *) malloc(size * sizeof(int));',
    (4, 5): 'scanf("d", &kind)',
    (5, 6): 'kind != EOF',
    (5, 30): 'kind == EOF',
    (6, 7): 'kind == 0',
    (7, 8): 'top >= size',
    (8, 9): 'fprintf(stderr, "fatal error stack overflow");',
    (9, 30): 'exit(1);',
    (7, 10): 'top < size',
    (10, 11): 'fprintf(stderr, "enter data to push");',
    (11, 12): 'scanf("d", &data);',
    (12, 13): 'stack[top] = data',
    (13, 14): 'top = top + 1',
    (14, 4): 'break',
    (6, 15): 'kind == 1',
    (15, 16): 'top <= 0',
    (16, 17): 'fprintf(stderr, "fatal error stack underflow")',
    (17, 30): 'exit(2)',
    (15, 18): 'top > 0',
    (18, 19): 'top = top - 1',
    (19, 20): 'printf("top of the stack is d", stack[top])',
    (20, 4): 'break',
    (6, 21): 'kind == 2',
    (21, 22): 'i = 0',
    (22, 23): 'i < top',
    (23, 24): 'printf("stack d =d", i, stack[i])',
    (24, 22): 'i = i + 1',
    (22, 25): 'i >= top',
    (25, 4): 'break',
    (6, 26): 'default',
    (26, 27): 'fprintf(stderr, "fatal error unknown operation")',
    (27, 30): 'exit(3)',
    (28, 4): 'break',
    }  # for debugging

combiners = {    
    0: [State.join,State.join],
    1: [State.join,State.join],
    2: [State.join,State.join],
    3: [State.join,State.join],
    4: [State.widening,State.narrowing],
    5: [State.join,State.join],
    6: [State.join,State.join],
    7: [State.join,State.join],
    8: [State.join,State.join],
    9: [State.join,State.join],
    10: [State.join,State.join],
    11: [State.join,State.join],
    12: [State.join,State.join],
    13: [State.join,State.join],
    14: [State.join,State.join],
    15: [State.join,State.join],
    16: [State.join,State.join],
    17: [State.join,State.join],
    18: [State.join,State.join],
    19: [State.join,State.join],  
    20: [State.join,State.join],
    21: [State.join,State.join],
    22: [State.widening,State.narrowing],
    23: [State.join,State.join],
    24: [State.join,State.join],
    25: [State.join,State.join],
    26: [State.join,State.join],
    27: [State.join,State.join],
    28: [State.join,State.join],
    29: [State.join,State.join],
    30: [State.join,State.join],
}

chaotic_ex(succ, 0, iota, combiners, bottom, tr, tr_txt, "a2dynamic.png")


"""   
   //* Initializations */
0      top = 0 ;
1      fprintf(stderr, "enter maximum stack's size\n");
2      scanf("%d", &size);

3      stack = (int *) malloc(size * sizeof(int));

       /* Main loop */
4,5    while (scanf("%d", &kind) != EOF) {
6        switch(kind) {
        case 0: // push
7            if ( top >= size ) {
8                fprintf(stderr, "fatal error: stack overflow\n");
9                exit(1);
             }
10           fprintf(stderr, "enter data to push\n");
11           scanf("%d", &data);
12           stack[top] = data;
13           top = top + 1 ;
14           break;
         case 1: // pop
15           if (  top <= 0) {
16               fprintf(stderr, "fatal error: stack underflow\n");
17               exit(2);
           }
18           top = top - 1 ;
19           printf("top of the stack is %d\n", stack[top]) ;
20           break;
       case 2: // print
21           i = 0 ;
22           while (i < top ) {
23               printf("stack[%d]=%d\n", i, stack[i]);
24               i = i + 1 ;
           }
25           break;

       default: 
26           fprintf(stderr, "fatal error: unknown operation\n");           
27           exit(3);
28           break ;
       }
   }
}
"""